\begin{tabbing}
es{-}first{-}at{-}since'(${\it es}$;$i$;$e$;$e$.$R$($e$);$e$.$P$($e$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=loc($e$) = $i$\+
\\[0ex]\& $R$($e$)
\\[0ex]\& ($\exists$\=${\it e'}$:E\+
\\[0ex]((${\it e'}$ $<$loc $e$) c$\wedge$ ($P$(${\it e'}$) \& ($\forall$${\it e''}$:E. ${\it e'}$ $\leq$loc ${\it e''}$  $\Rightarrow$ (${\it e''}$ $<$loc $e$) $\Rightarrow$ ($\neg$$R$(${\it e''}$))))))
\-\-
\end{tabbing}